alle{-}at1(${\it es}$; $i$; $x$; $x$.$P$($x$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$alle{-}at(${\it es}$;$i$;$e$.$P$(es{-}when(${\it es}$; $x$; $e$)))